SWellFounded(R(x;y)) == f:(T). x, y:T. R(x;y)  f(x)<f(y) 

latex

---

clarification:

strongwellfounded(T; x,y.R(x;y)) == f:(T). x:T, y:T. R(x;y)  f(x)<f(y) 

latex

Definitions	x:A. B(x), x:AB(x), , x:A. B(x), P  Q, a<b, f(a)
FDL editor aliases	strongwellfounded